All good suggestions... and I've a long train journey tomorrow...

Aaargh. More branch merge nonsense. Will revert. Blast!
Still didn't nail it down. Grrr... trying to do too much, too quickly.
Try again tomorrow!

Yup it looks like the merge has gone wrong again. It seems to be a similar problem each time. What is the series of commands you're using to merge?

Matthew, it seems to be a combination of things:

• first fatal mistake: doing too many things at once, and doing them while too tired to concentrate;
• having two copies of the same branch on two different local machines, each pushing to a single remote branch on jamesmckinna/agda-stdlib;
• the two copies having out-of-sync versions of the agda:master branch from which they were (originally) derived;
• pushing from one local to the remote, and then pulling from there to the other
• generating an explicit merge-commit cycle, (at which point everything is in fact screwed up)
• compounding the error by pushing to the remote
• now, the third, 'unbroken' local branch can't be pushed to the remote because of the push/pull merge conflict this has generated

There are then second-order effects arising from (still!) not getting right how to revert such changes far enough back to undo the mess, and then re-committing the 'good' commits---I seem always to be off-by-one in one direction of time or the other.

I'm snowed under with other things right now, so it will be next week now before I dig my way back out of this one. One copy I have is still (relatively) clean, so I may simply push commits from there to a fresh branch. Sorry that this will screw up the reviewing, but it seems more reliable than trying to fix up a broken tree on the remote branch. But I will also investigate that as well.

I should by now have learnt that being prompted to record a merge commit message is sign of doing something wrong; if I I fetch before attempting to merge (ie don't pull, only fetch), can I somehow preview what will happen and forestall this kind of screw-up again?

OK... @MatthewDaggitt can you review the latest round of commits to make sure that this is OK... there still seem to be some spurious commits associated with CHANGELOG1.7.2, but I haven't been able to track those down to eliminate them :-(

It appears I have (once again: time to put me out to pasture, perhaps) reverted an irrelevant change, in this case Jacques' "minor whitespace violation" #1922 . Any way, when merging the present branch, to avoid these two? Sigh...

UPDATED: OK, hopefully that last commit really should be the last...

Thanks @MatthewDaggitt but I think you should have squashed those commits... they each seem to have contributed to my tally on the contributors page, which is the wrong arithmetic, i think.